Nuprl Lemma : inv_image_ind
13,42
postcript
pdf
A
:Type,
r
:(
A
A
),
B
:Type,
f
:(
B
A
).
WellFnd{i}(
A
;
x
,
y
.
r
(
x
,
y
))
WellFnd{i}(
B
;
x
,
y
.
r
(
f
(
x
),
f
(
y
)))
latex
Up
well
fnd
,
well
fnd
Lemmas
inv
image
ind
tp
origin
A:Type, r:(A
A
), B:Type, f:(BA).
WellFnd{i}(B;x,y.r(f(x),f(y))) A:Type, r:(AA), B:Type, f:(BA).
WellFnd{i}(B;x,y.r(f(x),f(y)))